package model.cnf;
import java.io.File;
import java.io.IOException;
import java.util.List;


/**
 * represet a CNF
 * @author stephane
 *
 */
public abstract class CNF{
	public static final String PREFIX = "";
	public static final String SUFFIX = ".export.cnf";
	
	//aide a la lecture de CNF dans un fichier
	public static final char COMMENTAIRE = 'c';


	public static final char DESCRIPTION = 'p';
	public static final int SIZE_DESCRIPTION = 5;
	
	protected File CNFfile;
	protected int declaredNumVar;
	protected int declaredNumClause;
	protected boolean modify = false;
	

	protected Stat stat;

	
	public int getDeclaredNumVar() {
		return declaredNumVar;
	}

	public int getDeclaredNumClause() {
		return declaredNumClause;
	}
	
	public boolean isModify() {
		return modify;
	}

	public void setModify(boolean modify) {
		this.modify = modify;
	}


	public String getFileName() {
		return CNFfile.getName();
	}

	public Stat getStat() {
		return stat;
	}

	public void setStat(Stat stat) {
		this.stat = stat;
	}
	
	public abstract void checkStat() throws Exception;

	public File getCNFfile() {
		return CNFfile;
	}

	public int size(){
		return declaredNumClause;
	}
		
	public int getNumVar() throws Exception{
		return declaredNumVar;
	}
	
	/**
	 * export the CNF in File format
	 * @param cnf pathname of the file
	 * @param directory the directory to save the CNF
	 * @return the file
	 */
	public abstract File export(String cnf, File directory);

	/**
	 * export the CNF in File format
	 * @param directory the directory to save the CNF
	 * @return the file
	 */
	public abstract File export(File directory);

	/**
	 * return all the clause of the CNF
	 * @return all the clause of the CNF
	 * @throws Exception
	 */
	public abstract List<Clause> getClauses() throws Exception;
	
	/**
	 * check the CNF for modification 
	 * @throws Exception
	 */
	public abstract void check() throws Exception;
	
	
	/**
	 * add a list of clause to the CNF
	 * @param cl the list clause to add
	 */
	public abstract void addClause(List<Literal> cl);
	
	/**
	 * add a clause to the CNF
	 * @param cl the clause to add
	 */	
	public abstract void addClause(Clause cl);
	
	/**
	 * get clause number "i" in the CNF
	 * @param i the number of the clause
	 * @return the clause number "i"
	 * @throws IOException if something goes wrong with the file
	 * @throws IllegalArgumentException if the clause "i" doen't exist
	 */
	public abstract Clause getClause(int i) throws IllegalArgumentException, IOException;

		
}